Issue1963MagicWith.agda:30,1-31,16
p .proj₁ != w of type Nat
when checking that the type
(p : Σ Nat IsZero) (w : Nat) → F w (p .proj₂) of the generated with
function is well-formed
